Nuprl Definition : d-world 11,40

d-world(D;v;sched;dec;discrete)
== <i,x. M(i).ds(x)
== , i,a. M(i).da(locl(a))
== , l,tg. M(source(l)).dout(l,tg)
== , i,t. if (t = 0)
== then x.M(i).init(x)?v(i,x)
== else (CV(d-comp(D; v; sched; dec; discrete))((t - 1),i)).1
== fi 
== , i,t. ((CV(d-comp(D; v; sched; dec; discrete))(t,i)).2).1
== , i,t. (CV(d-comp(D; v; sched; dec; discrete))(t,i)).2.2
== , i.d-machine(i;M(i);dec(i))
== , discrete
== , > 
latex



clarification:

d-world{i:l}
d-world(D; v; sched; dec; discrete)
== <i,x. d-m(D; i).ds(x)
== , i,a. d-m(D; i).da(locl(a))
== , l,tg. d-m(D; source(l)).dout(l,tg)
== , i,t. if (t = 0)
== then x.d-m(D; i).init(x)?v(i,x)
== else (CV(d-comp(D; v; sched; dec; discrete))((t - 1),i)).1
== fi 
== , i,t. ((CV(d-comp(D; v; sched; dec; discrete))(t,i)).2).1
== , i,t. (CV(d-comp(D; v; sched; dec; discrete))(t,i)).2.2
== , i.d-machine(i;d-m(D; i);dec(i))
== , discrete
== , > 
latex


DefinitionsM.ds(x), M.da(a), locl(a), M.dout(l,tg), source(l), if b then t else f fi , (i = j), M.init(x)?v, n - m, #$n, t.1, t.2, CV(F), d-comp(D; v; sched; dec; d), x.A(x), d-machine(i;M;dec), M(i), f(a), <a, b>,
FDL editor aliasesd-world

origin